y=f*(x) via L
== (0 < ||L||)
== & y = hd(L)
== & x = last(L)
== & (i:{0..(||L|| - 1)}. L[i] = f(L[(i+1)]) & ((L[i] = L[(i+1)]))) 

latex

---

clarification:

fun-path(T;f;L;y;x)
== (0 < ||L||)
== & y = hd(L)  T
== & x = last(L)  T
== & (i:{0..(||L|| - 1)}. L[i] = f(L[(i+1)])  T & ((L[i] = L[(i+1)]  T))) 

latex

Definitions	a < b, hd(l), last(L), x:A. B(x), {i..j}, n - m, ||as||, P & Q, f(a), A, s = t, l[i], n+m, #$n
FDL editor aliases	fun-path